# Copyright 2024 Google LLC
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
#      http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

# This file contains build rules for the main binary of p4_symbolic.

package(
    default_visibility = ["//visibility:public"],
    licenses = ["notice"],
)

cc_binary(
    name = "main",
    srcs = [
        "main.cc",
    ],
    deps = [
        ":test_util",
        "//gutil/gutil:io",
        "//p4_pdpi/internal:ordered_map",
        "//p4_symbolic/symbolic",
        "//p4_symbolic/symbolic:solver_state",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_google_absl//absl/flags:flag",
        "@com_google_absl//absl/flags:parse",
        "@com_google_absl//absl/flags:usage",
        "@com_google_absl//absl/log",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/strings:str_format",
        "@com_google_protobuf//:protobuf",
    ],
)

cc_library(
    name = "z3_util",
    srcs = ["z3_util.cc"],
    hdrs = ["z3_util.h"],
    deps = [
        "//gutil/gutil:status",
        "//p4_pdpi/string_encodings:bit_string",
        "//p4_pdpi/string_encodings:hex_string",
        "@com_github_z3prover_z3//:api",
        "@com_gnu_gmp//:gmp",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/status",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
        "@com_google_absl//absl/types:optional",
    ],
)

cc_library(
    name = "test_util",
    testonly = False,
    srcs = ["test_util.cc"],
    hdrs = ["test_util.h"],
    deps = [
        "//gutil/gutil:io",
        "//gutil/gutil:proto",
        "@com_github_p4lang_p4runtime//:p4info_cc_proto",
        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
        "@com_google_absl//absl/status:statusor",
        "@com_google_absl//absl/strings",
    ],
)

cc_test(
    name = "z3_util_test",
    srcs = ["z3_util_test.cc"],
    deps = [
        ":z3_util",
        "//gutil/gutil:status_matchers",
        "//p4_pdpi/string_encodings:bit_string",
        "@com_github_z3prover_z3//:api",
        "@com_google_absl//absl/numeric:int128",
        "@com_google_absl//absl/status",
        "@com_google_googletest//:gtest_main",
    ],
)
